package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class ChoosePay {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Choose; Pay");
		 
		 //Clocks
		 tiosts.addClock("clockC");
		 tiosts.addClock("clockP");
		 
         // Variables
         TypedData optionC = new TypedData("optionC", Constants.TYPE_INTEGER);
         tiosts.addVariable(optionC);
         TypedData optionP = new TypedData("optionP", Constants.TYPE_INTEGER);
         tiosts.addVariable(optionP);
         TypedData signature = new TypedData("signature", Constants.TYPE_BOOLEAN);
         tiosts.addVariable(signature);
         
         // Parameters
         TypedData op = new TypedData("op", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(op);
         TypedData info = new TypedData("info", Constants.TYPE_BOOLEAN);
         tiosts.addActionParameter(info);
         
         // Input, output, and internal actions
         Action init = new Action("initC", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
         Action select = new Action("select", Constants.ACTION_INPUT);
         select.addParameter(op.getName());
         tiosts.addAction(select);
         Action returnAction = new Action("return", Constants.ACTION_OUTPUT);
         tiosts.addAction(returnAction);
         Action performPayment = new Action("performPayment", Constants.ACTION_OUTPUT);
         tiosts.addAction(performPayment);
         Action shutdown = new Action("shutdown", Constants.ACTION_OUTPUT);
         tiosts.addAction(shutdown);
         Action send = new Action("send", Constants.ACTION_OUTPUT);
         send.addParameter(op.getName());
         tiosts.addAction(send);
         Action sign = new Action("sign", Constants.ACTION_INPUT);
         sign.addParameter(info.getName());
         tiosts.addAction(sign);
         Action discard = new Action("discard", Constants.ACTION_OUTPUT);
         tiosts.addAction(discard);
         Action pay = new Action("pay", Constants.ACTION_OUTPUT);
         tiosts.addAction(pay);
         Action finishSystem = new Action("finishSystem", Constants.ACTION_OUTPUT);
         tiosts.addAction(finishSystem);
         
         // Locations
         Location start = new Location("StartC");
         tiosts.addLocation(start);
         Location s0 = new Location("S0");
         tiosts.addLocation(s0);
         Location s1 = new Location("S1");
         tiosts.addLocation(s1);     
         Location s3s6 = new Location("S3,S6");
         tiosts.addLocation(s3s6); 
         Location s2s5 = new Location("S2,S5");
         tiosts.addLocation(s2s5);   
         Location s7 = new Location("S7");
         tiosts.addLocation(s7);  
         Location s8 = new Location("S8");
         tiosts.addLocation(s8); 
         Location s9 = new Location("S9");
         tiosts.addLocation(s9);
         Location s10 = new Location("S10");
         tiosts.addLocation(s10); 
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("StartC", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S0");
         tiosts.createTransition("S0",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, select, "optionC := op", null, Constants.DEADLINE_LAZY, "S1");
         //cash = 1   card = 2  check = 3 off = 4
         tiosts.createTransition("S1",  "optionC = 1 OR optionC = 2 OR optionC = 3", "clockC <= 10", performPayment, null, null, Constants.DEADLINE_LAZY, "S2,S5");
         tiosts.createTransition("S1",  "optionC = 4", "clockC <= 10", shutdown, null, null, Constants.DEADLINE_LAZY, "S2,S5");
         tiosts.createTransition("S1",  Constants.GUARD_TRUE, "clockC > 10", returnAction, null, "clockC := 0", Constants.DEADLINE_LAZY, "S0");
         tiosts.createTransition("S2,S5", "optionC = op", Constants.GUARD_TRUE, send, "optionP := op", null, Constants.DEADLINE_EAGER, "S3,S6");
         //cash = 1   card = 2  check = 3 off = 4
         tiosts.createTransition("S3,S6",  "optionP = 1 OR optionP = 3", "clockP <= 20", pay, null, null, Constants.DEADLINE_LAZY, "S7");
         tiosts.createTransition("S3,S6",  "optionP = 4", Constants.GUARD_TRUE, finishSystem, null, null, Constants.DEADLINE_LAZY, "S8");
         tiosts.createTransition("S3,S6",  "optionP = 2", "clockP <= 20", sign, "signature := info", null, Constants.DEADLINE_LAZY, "S9");
         tiosts.createTransition("S9",  "signature <=>  FALSE", Constants.GUARD_TRUE, discard, null, "clockP := 0", Constants.DEADLINE_LAZY, "S3,S6");
         tiosts.createTransition("S9", "signature <=> TRUE", Constants.GUARD_TRUE, pay, null, null, Constants.DEADLINE_LAZY, "S10");
         //tiosts.createTransition("S9",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, discard, null, "clockP := 0", Constants.DEADLINE_LAZY, "S3,S6");
         //tiosts.createTransition("S9", Constants.GUARD_TRUE, Constants.GUARD_TRUE, pay, null, null, Constants.DEADLINE_LAZY, "S10");
         
         return tiosts;		 
	 }

}
